i:Id, k:Knd, l:IdLnk, ds:x:Id fp Type, da:a:Knd fp Type,
f:(tg:Id(State(ds)Valtype(da;k)(da(rcv(l,tg))?Void List))) List.
source(l) = i
 @i: with declarations 
 ds:ds
 da:da
 dk(v) sends f s v on link l 
 realizes es.
 (x:Id. vartype(i;x)  ds(x)?Top) & (e:E. loc(e) = i  Id  valtype(e)  Valtype(da;kind(e)))
 & (e:E. isrcv(e)  lnk(e) = l  IdLnk  valtype(e)  Valtype(da;kind(e)))
 & (e:E.
 & (loc(e) = i  Id
 & ( kind(e) = k  Knd
 & ( (L:{e':E| isrcv(e') & lnk(e') = l  IdLnk } List.
 & ( ((e':E. (e'  L)  isrcv(e') & lnk(e') = l  IdLnk & sender(e') = e  E)
 & ( (& (e1, e2:E. e1 before e2  L  (e1 <loc e2))
 & ( (& map(e'.<tag(e'),val(e')>;L)
 & ( (& =
 & ( (& tagged-list-messages(z.z when e;val(e);f)
 & ( (&  (tg:IdValtype(da;rcv(l,tg))) List)) 

latex

Definitions

x:A. B(x), P  Q, D realizes es. P(es), A & B, P & Q, t  T, Prop, x. t(x), x:A. B(x), P  Q, P  Q, S  T, S  T, T, True, SQType(T), {T}, , P  Q, State(ds), AB, A, False, Top, tagged-messages(l;s;v;L), f o g, 2of(t), Valtype(da;k), map(f;as), Y, mlnk(m), 1of(t), haslink(l;m), {i..j}, i  j < k, msg(l;t;v), (Msg on l), x(s), SqStable(P), Msg(M)

Lemmas

sends-rule, Knd wf, es-kind wf, w-es wf, Id wf, es-loc wf, es-E wf, possible-world wf, fair-fifo wf, world wf, d-sub wf, d-single-sends wf, dsys wf, lsrc wf, ma-state wf, ma-valtype wf, fpf-cap wf, Kind-deq wf, rcv wf, fpf wf, IdLnk wf, es-axioms, map wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, assert wf, es-isrcv wf, es-lnk wf, pi1 wf, es-sender wf, es-index wf, upto wf, non neg length, l member wf, member map, sq stable from decidable, decidable assert, IdLnk sq, subtype rel self, member upto2, le wf, ldst wf, es-locl-antireflexive, es-locl wf, l before wf, before-map, before-upto, es-val wf, Knd sq, es-when wf, es-vartype wf, id-deq wf, top wf, list-eq-set-type, Msg wf, mlnk wf, select wf, map-map, tagged-list-messages wf, fpf-cap-void-subtype, list extensionality, es-tag wf, mlnk wf2, length-map, length upto, select-map, select upto, es-Msg wf, squash wf, true wf, event system wf, pi2 wf, iff wf, sq stable subtype rel, es-valtype wf, subtype rel wf